Nuprl Lemma : ecl-trans-state-from_wf 11,40

ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), v:ecl-trans-tuple{i:l}(dsda), z:ecl-trans-type(v),
L:(event-info(ds;da) List). ecl-trans-state-from(vzL ecl-trans-type(v
latex


Definitionst  T, ma-valtype(dak), Kind-deq, Knd, x:AB(x), (x  l), b, prop{i:l}, A, b, , deq-member(eqxL), P  Q, P  Q, P  Q, Unit, event-info(ds;da), decl-state(ds), top, fpf-cap(feqxz), if b then t else f fi , x,yt(x;y), list_accum(x,a.f(x;a); yl), spreadn(ua,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-state-from(vzL), ecl-trans-type(A), ecl-trans-tuple{i:l}(dsda), Id, xt(x), fpf(Aa.B(a))
Lemmasecl-trans-type wf, ecl-trans-tuple wf, fpf wf, Id wf, list accum wf, ifthenelse wf, event-info wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, l member wf, Knd wf, Kind-deq wf

origin